lean 4エラーメモ
code:memo
⋊> /V/e/w/g/l/l/my-lean-proj on main ⨯ lake update
error: ./lean_packages/mathlib/lakefile.lean:7:2: error: unknown attribute default_target error: ./lean_packages/mathlib/lakefile.lean:11:2: error: unknown attribute default_target error: ./lean_packages/mathlib/lakefile.lean: package configuration has errors
⋊> /V/e/w/g/l/l/my-lean-proj on main ⨯ lake update
mathlib: no manifest entry; deleting ./lean_packages/mathlib and cloning again
error: ./lean_packages/mathlib/lakefile.lean:7:2: error: unknown attribute default_target error: ./lean_packages/mathlib/lakefile.lean:11:2: error: unknown attribute default_target error: ./lean_packages/mathlib/lakefile.lean: package configuration has errors
code:memo
c:\Users\alles\.elan\toolchains\leanprover--lean4---nightly-2023-06-08\bin\lake.exe print-paths Init failed:
stderr:
error: .\lakefile.lean:4:8: error: expected identifier
error: .\lakefile.lean:8:9: error: expected identifier
error: .\lakefile.lean:13:9: error: expected identifier
error: .\lakefile.lean: package configuration has errors
Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.
下のサンプルを参考にした方が良い。
============================
code:memo
PS D:\workspace\ghworkspace\language\lean\my-lean-proj> lake update
updating lake-packages\mathlib to revision bca93b9f1fa478d202d51efe98b90d3678695209
error: .\lake-packages\mathlib\lakefile.lean:31:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: .\lake-packages\mathlib\lakefile.lean:57:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: .\lake-packages\mathlib\lakefile.lean: package configuration has errors
なんもわからん。